\begin{tabbing}
$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}).
\\[0ex]($\forall$$x$:$T$. $\neg$$R$($x$,$x$))
\\[0ex]$\Rightarrow$ ($\forall$$x$,$y$:$T$. $R$($x$,$y$) $\Rightarrow$ ($\neg$$R$($y$,$x$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it as}$,${\it bs}$:($T$ List).\+
\\[0ex]l{-}ordered($T$; $x$,$y$.$R$($x$,$y$); ${\it as}$)
\\[0ex]$\Rightarrow$ l{-}ordered($T$; $x$,$y$.$R$($x$,$y$); ${\it bs}$)
\\[0ex]$\Rightarrow$ ((${\it as}$ = ${\it bs}$) $\Leftarrow\!\Rightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ ${\it as}$) $\Leftarrow\!\Rightarrow$ ($x$ $\in$ ${\it bs}$))))
\-
\end{tabbing}